;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(interface iHelpers
  (sig RGB-to-HSV (r g b))
  (sig HSV-to-RGB (h s v))
  
  ; RGB-to-HSV returns a list of three numbers:
  ; rational h [0, 360], rational s [0, 1], rational v [0, 255]
  (con rgb-to-hsv-returns-list-of-3
       (implies (and (and (natp r) (<= r 255))
                     (and (natp g) (<= g 255))
                     (and (natp b) (<= b 255)))
                (let* ((hsv (RGB-to-HSV r g b))
                       (h   (car hsv))
                       (s   (cadr hsv))
                       (v   (caddr hsv)))
                  (and (and (consp hsv) (= (len hsv) 3))
                       (and (natp h) (<= h 360))
                       (and (rationalp s) (>= s 0) (<= s 1))
                       (and (natp v) (<= v 255))))))
  
  ; HSV-to-RGB returns a list of three numbers between [0, 255]
  (con hsv-to-rgb-returns-list-of-3
       (implies (and (and (natp h) (<= h 360))
                     (and (rationalp s) (<= s 1) (>= s 0))
                     (and (natp v) (<= v 255)))
                (let* ((rgb (HSV-to-RGB h s v))
                       (r   (car rgb))
                       (g   (cadr rgb))
                       (b   (caddr rgb)))
                  (and (and (consp rgb) (= (len rgb) 3))
                       (and (natp r) (<= r 255))
                       (and (natp g) (<= g 255))
                       (and (natp b) (<= b 255)))))))